free theorem

参考

gpt-5.icon

多相型（parametric polymorphism）をもつ関数の「型」だけから、その関数が必ず満たす性質を導ける定理のことです。

実装を一切見なくても、型が制約として振る舞う点が本質です。

直観的な考え方

多相関数は「型に関して中立」でなければなりません。

つまり、

特定の型に依存した分岐ができない

値の中身を勝手に作れない（引数にあるものしか使えない）

この制約から、「どう振る舞うか」が型だけで決まります。

基本例

code:haskell

id :: forall a. a -> a

この型を持つ関数は何ができるか？

👉 結論

返せるのは「受け取った値そのもの」だけ。

free theorem

code:text

id x = x

code:haskell

この関数は、

👉 つまり：

要素数を勝手に増やせない

各要素に関数を適用する以外のことはできない

free theorem（直感的表現）

code:text

f g = map g ∘ f id

（実質「map的な構造保存」を強制される）

数学的な定式化（ざっくり）

free theorem は parametricity（パラメトリシティ） から導かれます。

関数を「関係を保存する写像」

と解釈すると、

多相関数は、すべての型の間の関係を壊さない

という性質が得られ、そこから等式（定理）が導出されます。

典型的な制約パターン

table:_

型 必然的な振る舞い

注意点

副作用（IO、例外）を含むと成立しない場合がある

純粋・parametric であることが前提

何がfreeなん？

これってfunctor即の話？

定理

code:hs

g . h = k . f

以下を満たす

code:hs

$map g . fmap h = fmap k . $map f

補題1

code:hs

fmap f = $map f

Functor則の1つ目と、free theoremから導出できる

補題2

code:hs

f . g = id . (f . g)

定理

code:hs

fmap f. fmap g = fmap (f . g)

証明

割と大変っぽい

code:hs

fmap id = id

fmap f . fmap g = fmap (f . g)

導出

https://gyazo.com/830db6c0e463c23342daec8794efc2ac

parametricだからこそ得られる性質である、的なことが書いてある